Definitions | False, P  Q, A, x:A. B(x), P & Q, b, t T, IdLnk, x:A B(x), Id, Knd, x:A B(x), Void, Type, x.A(x),  x. t(x), 2of(t), IdDeq, f(x)?z, Top, 1of(t), KindDeq, State(ds), a:A fp B(a), product-deq(A;B;a;b), x dom(f), x dom(f). v=f(x)  P(x;v), M.da(a), M.state, M.rframe(A.sends tfL of k on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), Feasible(M), Valtype(da;k), MsgA, <a,b> |